package propcalc_lang.tests;

import java.util.*;

import junit.framework.TestCase;
import propcalc_lang.ast.*;
import propcalc_lang.parser.ParserCup;

public class PatternMatchingTests extends TestCase {

	private Proposition parseProp(String text) throws Exception {
		return (Proposition)ParserCup.parseString(text);
	}
	
	public void testVariables() throws Exception {
		Set<String> vars;
	// Without variables.
		vars = parseProp("true").variables(new HashSet<String>());
		assertTrue(vars.isEmpty()); 
		vars = parseProp("true & false").variables(new HashSet<String>());
		assertTrue(vars.isEmpty());
	// With variables.
		vars = parseProp("a").variables(new HashSet<String>());
		assertTrue(vars.contains("a"));
		assertEquals(1, vars.size());
		vars = parseProp("a & b").variables(new HashSet<String>());
		assertTrue(vars.contains("a"));
		assertTrue(vars.contains("b"));
		assertEquals(2, vars.size());
		vars = parseProp("a & true").variables(new HashSet<String>());
		assertTrue(vars.contains("a"));
		assertEquals(1, vars.size());
	}
	
	public void testSubstitution() throws Exception {
		Map<String, Proposition> replacements = new HashMap<String, Proposition>();
		replacements.put("t", parseProp("true"));
		replacements.put("f", parseProp("false"));
		replacements.put("a", parseProp("true & false"));
		replacements.put("o", parseProp("true | false"));
		assertEquals("true",
			parseProp("t").substitution(replacements).unparse());
		assertEquals("false",
				parseProp("f").substitution(replacements).unparse());
		assertEquals("(! true)",
				parseProp("!t").substitution(replacements).unparse());
		assertEquals("(false & true)",
				parseProp("f & t").substitution(replacements).unparse());
		assertEquals("(false | true)",
				parseProp("f | t").substitution(replacements).unparse());
		assertEquals("(false xor false)",
				parseProp("f xor f").substitution(replacements).unparse());
		assertEquals("(true -> true)",
				parseProp("t -> t").substitution(replacements).unparse());
		assertEquals("(false <-> true)",
				parseProp("f <-> t").substitution(replacements).unparse());
	}
	
	public void testRandomMatches() throws Exception {
		Random random = new Random(123456L);
		Map<String, Proposition> replacements1, replacements2;
		Proposition base, substitution;
		
		for (int i = 0; i < 30; i++) {
			base = Proposition.generate(random, 0, 3);
			replacements1 = new HashMap<String, Proposition>();
			for (String id : base.variables(new HashSet<String>())) {
				replacements1.put(id, Proposition.generate(random, 1, 2));
			}
			substitution = base.substitution(replacements1);
			replacements2 = new HashMap<String, Proposition>();
			assertTrue("Matching\n "+ substitution.unparse() +"\n with\n "+ base.unparse() +"\n failed.",
					substitution.match(base, replacements2));
		}
	}
}
